The talk will discuss recent advances in formalization of mathematics in proof assistants. We will briefly mention some recently finished large formalizations and systems such as the formal proof of the Kepler conjecture done in the HOL Light and Isabelle systems and the formal proof of the Odd Order theorem done in the Coq system. Then we will describe and demonstrate recent AI methods for reasoning and searching over large formal math corpora and also discuss emerging AI methods for automating the translation of informal mathematics to formal.